/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */


package ch.epfl.lara.patterns.utils;


import ch.epfl.lara.patterns.ast._

import collection.mutable.{Map,HashMap}

object FreshRenamer {

  type Subs = List[(String,String)] 
  
  import FreshNameCreator._
  
  
  def apply(matsch: Match): Match = {
    val Match((sname,stype),patterns) = matsch
    val newSname = fresh(sname)
    val substPatterns = patterns map (pattern => Substitution(makeSubs((sname,newSname) :: Nil, pattern), pattern)) 
    Match((newSname,stype), substPatterns)
  }

  
  
  def makeSubs(subst: Subs, pattern: Pattern): Subs = pattern match {
    case GuardedKlass(klass,guard) => 
      makeSubs(makeSubs(subst,klass.asInstanceOf[Pattern]), guard)
    
    case Klass(name,args) => 
      args.flatMap(arg => makeSubs(subst,arg)).removeDuplicates
      
    case _ => subst
  }
  

  def makeSubs(subst: Subs, arg: ArgPattern): Subs = arg match {
    case SimpleArgument(ident,typez) => 
      (ident,fresh(ident)) :: subst
    
    case klass @ _ if(klass.isInstanceOf[KlassPattern]) => makeSubs(subst,klass.asInstanceOf[Pattern])
  }
  
  
  def makeSubs(subst: Subs, guard: Guard): Subs = guard match {
    case Assume(f) => subst
  }
  
   
}
